Nuprl Definition : dist_1op_2op_lr 13,42
basic
Dist1op2opLR(A;1op;2op)
== u, v:A. 1op(u 2op v) = ((1op(u)) 2op v) & 1op(u 2op v) = (u 2op (1op(v))) 
latex

clarification:

basic
Dist1op2opLR(A;1op;2op)
== u:A, v:A. 1op(u 2op v) = ((1op(u)) 2op v)  A & 1op(u 2op v) = (u 2op (1op(v)))  A 
latex

Upgen algebra 1
Wellformedness Lemmasdist 1op 2op lr wf
Definitionsx:A. B(x), P & Q, x f y

origin